i, a:Id, T:Type, ds:x:Id fp Type, P:(State(ds)TProp),
init:{f:x:Id fp ds(x)?Void| x:Id. x  dom(ds)  x  dom(f) }.
Normal(T)
 Normal(ds)
 (s:State(ds). Dec(v:T. P(s,v)))
 R-Feasible(R-pre-init(i;ds;init;a;T;P)) 

latex

Definitions

x:A. B(x), Prop, P  Q, P  Q, x:A. B(x), t  T, x. t(x), P & Q, P  Q, R-Feasible(R), Top, True, f(x)?z, if b t else f fi, true, false, A || B, Y, Rplus?(x1), Rplus-left(x1), Rplus-right(x1), Rnone?(x1), R-loc(R), Rds(R), Rda(R), p = q, R-base-domain(R), R-frame-compat(A;B), R-interface-compat(A;B), p  q, i=j, 1of(t), p  q, 2of(t), Reffect?(x1), Rframe?(x1), Rframe-x(x1), Reffect-x(x1), Reffect-knd(x1), Rframe-L(x1), Raframe?(x1), Raframe-k(x1), Raframe-L(x1), Rrframe?(x1), Rrframe-x(x1), Reffect-ds(x1), Rrframe-L(x1), Rsends?(x1), Rsframe?(x1), Rsframe-lnk(x1), Rsends-l(x1), Rsframe-tag(x1), Rsends-g(x1), Rsends-knd(x1), Rsframe-L(x1), Rbframe?(x1), Rbframe-k(x1), Rbframe-L(x1), Rsends-ds(x1), Rpre?(x1), Rpre-ds(x1), Rpre-a(x1), Rsends-dt(x1), Reffect-T(x1), Rsends-T(x1), A & B, x(s), SQType(T), {T}, T, x  dom(f), xL. P(x), fpf-domain(f), R-pre-init(i;ds;init;a;T;P), Normal(T), Normal(ds), xdom(f). v=f(x)   P(x;v), , Unit, A, False, Id, a:A fp B(a),

Lemmas

decl-state wf, decidable wf, normal-ds wf, normal-type wf, fpf wf, Id wf, fpf-cap wf, id-deq wf, iff wf, assert wf, fpf-dom wf, fpf-trivial-subtype-top, Rall-nil, l all wf, Rall-cons, l all cons, R-compat-Rall, Rinit wf, fpf-ap wf, l member wf, bool wf, eqtt to assert, subtype rel self, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot, eq id wf, assert-eq-id, fpf-compatible-singles, Id sq, deq wf, fpf-empty-compatible-right, Knd wf, Kind-deq wf, fpf-empty wf, top wf, squash wf, true wf, not functionality wrt iff, all functionality wrt iff, deq-member wf, implies functionality wrt iff, assert-deq-member, Rpre wf, fpf-compatible-single-iff, fpf-single wf, locl wf